// Copyright 2019 - University of Strathclyde, King's College London and Schlumberger Ltd
// This source code is licensed under the BSD license found in the LICENSE file in the root directory of this source tree.

#include "typecheck.h"
#include "Exceptions.h"
#include "main.h"
#include "ptree.h"
#include <algorithm>
#include <functional>

namespace VAL {

  void TypeHierarchy::addDown(const PTypeRef &t1, const PTypeRef &t2) {
    GIC i = downGraph.find(&t1);
    GIC j = downGraph.find(&t2);
    if (i == downGraph.end()) {
      i = graph.find(&t1);
      downGraph[i->first] = Nodes();
    };
    if (j == downGraph.end()) {
      j = graph.find(&t2);
      downGraph[j->first] = Nodes();
      j = downGraph.find(&t2);
    };
    downGraph[&t1].insert(j->first);
  };

  TypeHierarchy::TypeHierarchy(const analysis *a) : leafNodes() {
    if (!a || !a->the_domain) {
      ParseFailure pf;
      throw(pf);
    };

    if (!a->the_domain->types) return;
    for (pddl_type_list::const_iterator i = a->the_domain->types->begin();
         i != a->the_domain->types->end(); ++i) {
      if ((*i)->type) {
        add(PTypeRef(*i), PTypeRef((*i)->type));
        addDown(PTypeRef((*i)->type), PTypeRef(*i));
      } else {
        if ((*i)->either_types) {
          for (pddl_type_list::const_iterator j = (*i)->either_types->begin();
               j != (*i)->either_types->end(); ++j) {
            add(PTypeRef(*i), PTypeRef(*j));
            addDown(PTypeRef(*j), PTypeRef(*i));
          };
        } else {
          PTypeRef pt(*i);
          Graph::iterator j = graph.find(&pt);
          if (j == graph.end()) {
            TypeRef *c = pt.clone();
            graph[c] = set< const TypeRef * >();
            downGraph[c] = set< const TypeRef * >();
          };
        };
      };
    };
  };

  TypeHierarchy::~TypeHierarchy() {
    for (Graph::const_iterator i = graph.begin(); i != graph.end(); ++i) {
      delete (i->first);
    };
  };

  /* gi is the Graph::iterator starting point aiming for t.
   * vs are the places visited so far.
   * gs is the original starting point.
   */

  bool TypeHierarchy::closure(Graph &gr, GI &gi, Nodes &vs, GI &gs,
                              const TypeRef *t) {
    if (gi == gr.end()) {
      return false;
    };
    if (*(gi->first) == *t) {
      for (Nodes::const_iterator i = vs.begin(); i != vs.end(); ++i) {
        gs->second.insert(*i);
        // insert(vs.begin(),vs.end());
      };
      // gs->second.insert(vs.begin(),vs.end());
      return true;
    };

    for (Nodes::iterator n = gi->second.begin(); n != gi->second.end(); ++n) {
      if (vs.find(*n) == vs.end()) {
        vs.insert(*n);
        GI tmp = gr.find(*n);
        if (closure(gr, tmp, vs, gs, t)) return true;
      };
    };
    return false;
  };

  vector< const pddl_type * > TypeChecker::leaves(const pddl_type *t) {
    typedef set< const TypeRef * > Nodes;
    PTypeRef pt(t);
    const Nodes &ns = th.leaves(pt);
    vector< const pddl_type * > vs(ns.size());

    int j = 0;
    for (Nodes::const_iterator i = ns.begin(); i != ns.end(); ++i, ++j) {
      vs[j] = ***i;
    };

    return vs;
  };

  bool TypeChecker::isLeafType(const pddl_type *t) {
    typedef set< const TypeRef * > Nodes;
    PTypeRef pt(t);
    return th.leaves(pt).empty();
  };

  vector< const pddl_type * > TypeChecker::accumulateAll(const pddl_type *t) {
    return th.accumulateAll(t);
  };

  vector< const pddl_type * > TypeHierarchy::accumulateAll(const pddl_type *t) {
    vector< const pddl_type * > nds(1, t);
    PTypeRef tt(t);
    GI gi = downGraph.find(&tt);
    if (gi == downGraph.end()) return nds;
    Nodes ns;
    PTypeRef pt(0);
    closure(downGraph, gi, ns, gi, &pt);
    for (Nodes::const_iterator i = ns.begin(); i != ns.end(); ++i) {
      nds.push_back(***i);
    };
    return nds;
  };

  const set< const TypeRef * > &TypeHierarchy::leaves(PTypeRef &t) {
    static Nodes empty;

    GI gi = leafNodes.find(&t);
    if (gi != leafNodes.end()) {
      return (gi->second);
    };

    gi = downGraph.find(&t);
    if (gi == downGraph.end()) return empty;
    Nodes ns;
    PTypeRef pt(0);
    closure(downGraph, gi, ns, gi, &pt);
    Nodes ms;
    for (Nodes::const_iterator i = ns.begin(); i != ns.end(); ++i) {
      Nodes xs;
      gi = downGraph.find(*i);
      closure(downGraph, gi, xs, gi, &pt);
      if (xs.empty()) ms.insert(*i);
    };
    leafNodes[downGraph.find(&t)->first] = ms;
    return leafNodes[downGraph.find(&t)->first];
  };

  void UTypeRef::addContents(TypeHierarchy *th) const {
    for (std::set< const pddl_type * >::const_iterator i = pts.begin();
         i != pts.end(); ++i) {
      th->add(PTypeRef(*i), *this);
    };
  };

  bool TypeHierarchy::reachable(const TypeRef &t1, const TypeRef &t2) {
    if (t1 == t2) return true;

    Graph::iterator i = graph.find(&t1);
    if (i == graph.end()) {
      return false;
    };

    Graph::const_iterator j = graph.find(&t2);
    if (j == graph.end() && t2.expected()) {
      return false;
    };
    t2.addContents(this);
    j = graph.find(&t2);

    if (i->second.find(j->first) != i->second.end()) return true;

    Nodes ns;
    return closure(graph, i, ns, i, j->first);
  };

  void TypeHierarchy::add(const PTypeRef &t1, const TypeRef &t2) {
    Graph::const_iterator i = graph.find(&t1);
    Graph::const_iterator j = graph.find(&t2);
    if (j == graph.end()) {
      TypeRef *c = t2.clone();
      graph[c] = set< const TypeRef * >();
      j = graph.find(&t2);
    };
    if (i == graph.end()) {
      TypeRef *c = t1.clone();
      graph[c] = set< const TypeRef * >();
    };
    graph[&t1].insert(j->first);
  };

  struct badchecker {
    TypeChecker *thea;

    badchecker(TypeChecker *a) : thea(a){};

    bool operator()(const operator_ *a) const {
      return !thea->typecheckAction(a);
    };
    bool operator()(const goal *g) const { return !thea->typecheckGoal(g); };
    bool operator()(const plan_step *p) {
      return !thea->typecheckActionInstance(p);
    };
    bool operator()(const effect *e) { return !thea->typecheckEffect(e); };
    bool operator()(const derivation_rule *d) {
      return !thea->typecheckDerivationRule(d);
    };
  };

  struct matchFunc {
    const func_symbol *f;

    matchFunc(const func_symbol *fs) : f(fs){};

    bool operator()(const func_decl *fd) const {
      if (!fd) {
        if (Verbose) *report << "Problematic function declaration!\n";
        ParseFailure pe;
        throw(pe);
      };
      const func_symbol *fdf = fd->getFunction();
      if (!fdf) {
        if (Verbose) *report << *fd << " problematic function declaration!\n";
        ParseFailure pe;
        throw(pe);
      };

      return f == fdf;
    };
  };

  struct matchPred {
    const pred_symbol *p;

    matchPred(const pred_symbol *ps) : p(ps){};

    bool operator()(const pred_decl *pd) const { return p == pd->getPred(); };
  };

  struct matchOp {
    const operator_symbol *f;

    matchOp(const operator_symbol *fs) : f(fs){};

    bool operator()(const operator_ *op) const { return f == op->name; };
  };

  struct matchSD {
    const operator_symbol *f;

    matchSD(const operator_symbol *fs) : f(fs){};

    bool operator()(const supplied_effect *se) const { return f == se->name; };
  };

  /* What does it all mean?
   *
   * Let c be a constant symbol, v a variable symbol and t be a type symbol.
   *
   * t1 - t2 means t1 is a subset of t2.
   * We allow multiple subset relations (multiple inheritance).
   * c - t means c is a member of t.
   * v - t means instantiations of v must be of type t.
   *
   * Therefore, subType(c - t1,v - t2) iff t1 - t2. Note that this relationship
   * might be via a path of transitive subset relations.
   *
   * v - (either t1 t2) is equivalent to v - (t1 U t2).
   * c - (either t1 t2) is not given a meaning, but we use the either field to
   * record multiple types for constants. Thus, c - t1 and c - t2 is legal and
   * is recorded internally using c - (either t1 t2). The meaning of the
   * multiple declarations is that c is of both types t1 and t2, so can be
   * substituted for any variable of either type. t - (either t1 t2) is also not
   * given a meaning (although the current parser will actually interpret it as
   * equivalent to "t - t1 t - t2").
   */

  bool TypeChecker::subType(const pddl_typed_symbol *tp1,
                            const pddl_typed_symbol *tp2) {
    if (!isTyped) return true;
    if (tp1->type) {
      if (tp2->type) {
        return th.reachable(PTypeRef(tp1->type), PTypeRef(tp2->type));
      } else {
        if (tp2->either_types) {
          return th.reachable(PTypeRef(tp1->type), UTypeRef(tp2->either_types));
        };
        if (Verbose) *report << tp2->getName() << " has bad type definition\n";
        TypeException te;
        throw(te);
      };
    } else {
      if (!tp1->either_types) {
        if (Verbose)
          *report << "Object with unknown type: " << tp1->getName() << "\n";
        TypeException te;
        throw(te);
      };

      // The situation is now complicated by the fact that variables and
      // constants must be treated differently. Constants have either types
      // representing conjunctions of types, while variables use them for
      // disjunctions.

      if (!tp1->either_types) {
        if (Verbose) *report << tp1->getName() << " badly typed!\n";
        TypeException te;
        throw(te);
      };

      if (dynamic_cast< const const_symbol * >(tp1)) {
        // The following confirms that a constant is a subtype of a given type
        // by checking that one of its types is appropriate.

        for (pddl_type_list::const_iterator i = tp1->either_types->begin();
             i != tp1->either_types->end(); ++i) {
          if (subType(*i, tp2)) return true;
        };
        return false;
      } else {
        for (pddl_type_list::const_iterator i = tp1->either_types->begin();
             i != tp1->either_types->end(); ++i) {
          if (!subType(*i, tp2)) return false;
        };
        return true;
      };
    };
  };

  bool TypeChecker::subType(const pddl_type *t, const pddl_typed_symbol *s) {
    if (!isTyped) return true;
    if (s->type) {
      return th.reachable(PTypeRef(t), PTypeRef(s->type));
    };

    if (!s->either_types) {
      if (Verbose) *report << s->getName() << " badly typed!\n";
      TypeException te;
      throw(te);
    };

    return th.reachable(PTypeRef(t), UTypeRef(s->either_types));
  };

  bool TypeChecker::subType(const pddl_type *t1, const pddl_type *t2) {
    if (!isTyped) return true;

    if (!t1 || !t2) {
      TypeException te;
      throw(te);
    };

    return th.reachable(PTypeRef(t1), PTypeRef(t2));
  };

  bool TypeChecker::typecheckProposition(const proposition *p) {
    if (!isTyped || !thea->the_domain->predicates) return true;
    pred_decl_list::const_iterator prd =
        std::find_if(thea->the_domain->predicates->begin(),
                     thea->the_domain->predicates->end(), matchPred(p->head));
    if (prd == thea->the_domain->predicates->end()) {
      if (p->head->getName() == "=") return true;
      if (Verbose)
        *report << "Predicate " << p->head->getName() << " not found\n";
      return false;
    };
    int idx = 1;

    var_symbol_list::const_iterator arg = (*prd)->getArgs()->begin();
    const var_symbol_list::const_iterator argEnd = (*prd)->getArgs()->end();

    parameter_symbol_list::const_iterator i = p->args->begin();
    const parameter_symbol_list::const_iterator e = p->args->end();

    for (; i != e && arg != argEnd; ++i, ++arg, ++idx) {
      if (!subType(*i, *arg)) {
        if (Verbose) {
          *report << "Type problem with proposition (";
          *report << p->head->getName();
          parameter_symbol_list::const_iterator it = p->args->begin();
          parameter_symbol_list::const_iterator et = p->args->end();
          for (; it != et; ++it) {
            *report << " " << (*it)->getName();
          }
          *report << ") - parameter " << idx << " is incorrectly typed\n";
        }
        return false;
      };
    };
    if (i != e) {
      if (Verbose) {
        *report << "Problem with proposition (";
        *report << p->head->getName();
        parameter_symbol_list::const_iterator it = p->args->begin();
        parameter_symbol_list::const_iterator et = p->args->end();
        for (; it != et; ++it) {
          *report << " " << (*it)->getName();
        }
        *report << ") - too many parameters\n";
      }
      return false;
    }

    if (arg != argEnd) {
      if (Verbose) {
        *report << "Problem with proposition (";
        *report << p->head->getName();
        parameter_symbol_list::const_iterator it = p->args->begin();
        parameter_symbol_list::const_iterator et = p->args->end();
        for (; it != et; ++it) {
          *report << " " << (*it)->getName();
        }
        *report << ") - too few parameters\n";
      }
      return false;
    }

    return true;
  };

  bool TypeChecker::typecheckFuncTerm(const func_term *ft) {
    if (!isTyped) return true;
    func_decl_list::const_iterator fd = std::find_if(
        thea->the_domain->functions->begin(),
        thea->the_domain->functions->end(), matchFunc(ft->getFunction()));
    const class_func_term *cft = dynamic_cast< const class_func_term * >(ft);

    if (fd == thea->the_domain->functions->end() && !cft) return false;
    if (cft) {
      // REMEMBER TO FIX THIS TO TYPECHECK PROPERLY
      return true;
    }
    var_symbol_list::const_iterator arg = (*fd)->getArgs()->begin();
    const var_symbol_list::const_iterator argEnd = (*fd)->getArgs()->end();
    parameter_symbol_list::const_iterator i = ft->getArgs()->begin();
    const parameter_symbol_list::const_iterator e = ft->getArgs()->end();
    int idx = 1;
    for (; i != e && arg != argEnd; ++i, ++arg, ++idx) {
      if (!subType(*i, *arg)) {
        if (Verbose) {
          *report << "Type problem with function term (";
          *report << ft->getFunction()->getName();
          parameter_symbol_list::const_iterator it = ft->getArgs()->begin();
          parameter_symbol_list::const_iterator et = ft->getArgs()->end();
          for (; it != et; ++it) {
            *report << " " << (*it)->getName();
          }
          *report << ") - parameter " << idx << " is incorrectly typed\n";
        }
        return false;
      };
    };
    if (arg != argEnd) {
      if (Verbose) {
        *report << "Problem with function term (";
        *report << ft->getFunction()->getName();
        parameter_symbol_list::const_iterator it = ft->getArgs()->begin();
        parameter_symbol_list::const_iterator et = ft->getArgs()->end();
        for (; it != et; ++it) {
          *report << " " << (*it)->getName();
        }
        *report << ") - too few parameters\n";
      }
    }
    if (i != e) {
      if (Verbose) {
        *report << "Problem with function term (";
        *report << ft->getFunction()->getName();
        parameter_symbol_list::const_iterator it = ft->getArgs()->begin();
        parameter_symbol_list::const_iterator et = ft->getArgs()->end();
        for (; it != et; ++it) {
          *report << " " << (*it)->getName();
        }
        *report << ") - too many parameters\n";
      }
    }

    return true;
  };

  bool TypeChecker::typecheckActionInstance(const plan_step *p) {
    if (!isTyped) return true;
    operator_list::const_iterator op =
        std::find_if(thea->the_domain->ops->begin(),
                     thea->the_domain->ops->end(), matchOp(p->op_sym));
    if (op == thea->the_domain->ops->end()) {
      pc_list< supplied_effect * >::const_iterator op1 = std::find_if(
          thea->the_problem->initial_state->supplied_effects.begin(),
          thea->the_problem->initial_state->supplied_effects.end(),
          matchSD(p->op_sym));
      return op1 != thea->the_problem->initial_state->supplied_effects.end();
    }
    var_symbol_list::const_iterator arg = (*op)->parameters->begin();
    const_symbol_list::const_iterator e = p->params->end();
    for (const_symbol_list::const_iterator i = p->params->begin(); i != e;
         ++i, ++arg) {
      if (!subType(*i, *arg)) {
        if (Verbose) *report << "Type problem in action " << *p << "\n";
        return false;
      };
    };
    return true;
  };

  bool TypeChecker::typecheckExpression(const expression *exp) {
    if (!isTyped) return true;
    if (const binary_expression *be =
            dynamic_cast< const binary_expression * >(exp)) {
      return typecheckExpression(be->getLHS()) &&
             typecheckExpression(be->getRHS());
    };
    if (const uminus_expression *ue =
            dynamic_cast< const uminus_expression * >(exp)) {
      return typecheckExpression(ue->getExpr());
    };
    if (const func_term *ft = dynamic_cast< const func_term * >(exp)) {
      return typecheckFuncTerm(ft);
    };
    return true;
  };

  bool TypeChecker::typecheckGoal(const goal *g) {
    if (!isTyped) return true;
    if (const preference *p = dynamic_cast< const preference * >(g)) {
      return typecheckGoal(p->getGoal());
    };
    if (const constraint_goal *cg =
            dynamic_cast< const constraint_goal * >(g)) {
      bool b1 = true;
      if (cg->getTrigger()) {
        b1 = typecheckGoal(cg->getTrigger());
      };
      return b1 && typecheckGoal(cg->getRequirement());
    };
    if (const simple_goal *sg = dynamic_cast< const simple_goal * >(g)) {
      return typecheckProposition(sg->getProp());
    };
    if (const conj_goal *cg = dynamic_cast< const conj_goal * >(g)) {
      if (cg->getGoals()->end() == std::find_if(cg->getGoals()->begin(),
                                                cg->getGoals()->end(),
                                                badchecker(this)))
        return true;
      return false;
    };
    if (const disj_goal *dg = dynamic_cast< const disj_goal * >(g)) {
      if (dg->getGoals()->end() == std::find_if(dg->getGoals()->begin(),
                                                dg->getGoals()->end(),
                                                badchecker(this)))
        return true;
      return false;
    };
    if (const imply_goal *ig = dynamic_cast< const imply_goal * >(g)) {
      return typecheckGoal(ig->getAntecedent()) &&
             typecheckGoal(ig->getConsequent());
    };
    if (const neg_goal *ng = dynamic_cast< const neg_goal * >(g)) {
      return typecheckGoal(ng->getGoal());
    };
    if (const timed_goal *tg = dynamic_cast< const timed_goal * >(g)) {
      return typecheckGoal(tg->getGoal());
    };
    if (const qfied_goal *qg = dynamic_cast< const qfied_goal * >(g)) {
      return typecheckGoal(qg->getGoal());
    };
    if (const comparison *c = dynamic_cast< const comparison * >(g)) {
      return typecheckExpression(c->getLHS()) &&
             typecheckExpression(c->getRHS());
    };
    if (const constraint_goal *cg =
            dynamic_cast< const constraint_goal * >(g)) {
      return (!cg->getRequirement() || typecheckGoal(cg->getRequirement())) &&
             (!cg->getTrigger() || typecheckGoal(cg->getTrigger()));
    };
    if (const named_goal *ng = dynamic_cast< const named_goal * >(g)) {
      return typecheckGoal(ng->gl);
    }
    return false;
  };

  bool TypeChecker::typecheckEffect(const effect *e) {
    if (!isTyped) return true;
    if (const simple_effect *se = dynamic_cast< const simple_effect * >(e)) {
      return typecheckProposition(se->prop);
    };
    if (const cond_effect *ce = dynamic_cast< const cond_effect * >(e)) {
      return typecheckGoal(ce->getCondition()) &&
             typecheckEffects(ce->getEffects());
    };
    if (const forall_effect *fe = dynamic_cast< const forall_effect * >(e)) {
      return typecheckEffects(fe->getEffects());
    };
    if (const timed_effect *te = dynamic_cast< const timed_effect * >(e)) {
      return typecheckEffects(te->effs);
    };
    if (const assignment *ass = dynamic_cast< const assignment * >(e)) {
      return typecheckFuncTerm(ass->getFTerm()) &&
             typecheckExpression(ass->getExpr());
    };
    return false;
  };

  bool TypeChecker::typecheckEffects(const effect_lists *es) {
    if (!isTyped) return true;
    return (es->add_effects.end() == std::find_if(es->add_effects.begin(),
                                                  es->add_effects.end(),
                                                  badchecker(this))) &&
           (es->del_effects.end() == std::find_if(es->del_effects.begin(),
                                                  es->del_effects.end(),
                                                  badchecker(this))) &&
           (es->forall_effects.end() == std::find_if(es->forall_effects.begin(),
                                                     es->forall_effects.end(),
                                                     badchecker(this))) &&
           (es->cond_effects.end() == std::find_if(es->cond_effects.begin(),
                                                   es->cond_effects.end(),
                                                   badchecker(this))) &&
           (es->assign_effects.end() == std::find_if(es->assign_effects.begin(),
                                                     es->assign_effects.end(),
                                                     badchecker(this))) &&
           (es->timed_effects.end() == std::find_if(es->timed_effects.begin(),
                                                    es->timed_effects.end(),
                                                    badchecker(this)));
  };

  bool TypeChecker::typecheckAction(const operator_ *act) {
    if (!isTyped) return true;
    //	Verbose = true;
    if (Verbose) *report << "Type-checking " << act->name->getName() << "\n";
    if (!typecheckGoal(act->precondition)) {
      if (Verbose) *report << "Conditions fail type-checking.\n";
      return false;
    }
    if (!typecheckEffects(act->effects)) {
      if (Verbose) *report << "Effects fail type-checking.\n";
      return false;
    }
    if (const durative_action *da =
            dynamic_cast< const durative_action * >(act)) {
      if (!typecheckGoal(da->dur_constraint)) {
        if (Verbose) *report << "Duration constraint fails type-checking.\n";
        return false;
      };
    };
    if (Verbose) *report << "...action passes type checking.\n";
    return true;
  };

  bool TypeChecker::typecheckDerivationRule(const derivation_rule *d) {
    if (!isTyped) return true;
    if (Verbose)
      *report << "Type-checking derivation rule for "
              << (d->get_head()->head->getName()) << "\n";
    pred_decl_list::iterator i = thea->the_domain->predicates->begin();
    for (; i != thea->the_domain->predicates->end(); ++i) {
      if ((*i)->getPred() == d->get_head()->head) {
        (*i)->setTypes(d->get_head());
        break;
      };
    };
    return i != thea->the_domain->predicates->end() &&
           typecheckGoal(d->get_body());
  };

  bool TypeChecker::typecheckDomain() {
    if (!isTyped) return true;
    return thea->the_domain->ops->end() ==
               std::find_if(thea->the_domain->ops->begin(),
                            thea->the_domain->ops->end(), badchecker(this)) &&
           thea->the_domain->drvs->end() ==
               std::find_if(thea->the_domain->drvs->begin(),
                            thea->the_domain->drvs->end(), badchecker(this)) &&
           (!thea->the_domain->constraints ||
            typecheckGoal(thea->the_domain->constraints));
  };

  bool TypeChecker::typecheckProblem() {
    if (!isTyped) return true;
    if (!thea || !thea->the_problem) {
      ParseFailure pf;
      throw(pf);
    };
    if (thea->the_problem->the_goal &&
        !typecheckGoal(thea->the_problem->the_goal)) {
      if (Verbose) *report << "Type-checking goal failed\n";
      return false;
    }
    if (!typecheckEffects(thea->the_problem->initial_state)) {
      if (Verbose) *report << "Type-checking initial state failed\n";
      return false;
    }
    if (thea->the_problem->constraints &&
        !typecheckGoal(thea->the_problem->constraints)) {
      if (Verbose) *report << "Type-checking constraints failed\n";
      return false;
    }
    return true;
  };

  bool TypeChecker::typecheckPlan(const plan *p) {
    if (!isTyped) return true;
    return p->end() == std::find_if(p->begin(), p->end(), badchecker(this));
  };

  vector< const_symbol * > TypeChecker::range(const var_symbol *v) {
    vector< const_symbol * > l;
    for (const_symbol_table::const_iterator i = thea->const_tab.begin();
         i != thea->const_tab.end(); ++i) {
      if (subType(i->second, v)) l.push_back(i->second);
    };

    return l;
  };

  vector< const_symbol * > TypeChecker::range(const parameter_symbol *v) {
    vector< const_symbol * > l;
    for (const_symbol_table::const_iterator i = thea->const_tab.begin();
         i != thea->const_tab.end(); ++i) {
      if (subType(i->second, v)) l.push_back(i->second);
    };

    return l;
  };

  vector< const_symbol * > TypeChecker::range(const pddl_type *t) {
    var_symbol v("");
    v.type = const_cast< pddl_type * >(t);  // OK - we will keep v const.
    v.either_types = 0;
    return range(&v);
  };

};  // namespace VAL
